COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	monadi[f83,jmc]		Normal form of monadic formulas
C00004 ENDMK
C⊗;
monadi[f83,jmc]		Normal form of monadic formulas

.require "memo.pub[let,jmc]" source;
.cb A NORMAL FORM FOR MONADIC FORMULAS AND SOME APPLICATIONS

."by John McCarthy, Stanford University"


	The following normal form theorem is related to the early work on
the decidability of monadic predicate calculus, but I haven't been able to
find it in the literature.  It has some interesting applications.

	Let %2P%51%*, . . . ,P%5n%1 be monadic predicate symbols and
let %2y%51%2,_._._._,y%5k%1 be individual variables.  When convenient
we group the %2P%1's and the %2y%1's into vectors  ⊗P  and ⊗y.  Let
⊗E(P,y)  be a formula involving these predicate symbols and free variables.

Theorem - Under the above hypotheses, ⊗E(P,y) is provably equivalent in
first order logic to a propositional formula whose constituents are

(i) the 2%4n%1 formulas  %2∃x.%AP